(* $Id: PFOLEnv.mli 204 2009-03-04 14:28:18Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

(** This module provides a typing environment for PFOL entities. It is
    used by the {!PFOLEncodedEnv} and {!PFOLEncoding} modules.
    Thus, its keys are identifiers of the {!XCoreSyntax module}. *)

open PFOLSyntax

(** The PFOL typing environment. *)
type env

(** The empty environment. *)
val empty : env

(** {1 Type variables} *)

(** Introduce a universally quantified type variable into the environment. *)
val introduce_rigid_type_variable :
  Position.t -> env -> XCoreSyntax.tid * XCoreSyntax.kind -> env

(** FIXME *)
val introduce_rigid_type_variables :
  Position.t -> env -> (XCoreSyntax.tid * XCoreSyntax.kind) list -> env

(** FIXME *)
val remove_rigid_type_variables : env -> XCoreSyntax.tid list -> env

(** FIXME *)
val lookup_type_variable : env -> XCoreSyntax.tid -> type_identifier

(** FIXME *)
val type_parameters : env -> XCoreSyntax.tid list -> type_identifier list

(** {1 Values} *)

(** FIXME *)
val bind_value :
  Position.t -> env -> XCoreSyntax.id -> type_scheme -> env * value_identifier

(** FIXME *)
val lookup : env -> XCoreSyntax.id -> value_identifier

(** FIXME *)
val type_of_id : env -> XCoreSyntax.id -> term_type

val remove_value : value_identifier -> env -> env

val remove_locals : Var.AtomSet.t -> env -> env

(** {1 Predicates} *)

(** FIXME *)
val bind_predicate :
  Position.t -> env -> XCoreSyntax.pid
  -> type_scheme -> predicate_declaration
  -> env * PFOLSyntax.Var.Atom.t * PFOLSyntax.Var.Atom.t

val is_predicate_object: env -> XCoreSyntax.pid -> bool

val is_predicate: env -> XCoreSyntax.pid -> bool

(** FIXME *)
val lookup_predicate : env -> XCoreSyntax.pid -> predicate_identifier

(** FIXME *)
val lookup_predicate_as_object : env -> XCoreSyntax.pid -> value_identifier

(** {1 Facts} *)

(** FIXME *)
val bind_fact : ?mark:string -> Position.t -> bool -> env -> predicate -> env

(** {1 Proof obligations} *)

val env_to_query : env -> Raw.query * Raw.query

val proof_obligation_to_query :
  ?filter:(string option -> bool) -> env -> predicate -> Raw.query * Raw.query
